
Load RCC axioms and inverses

Show tpp implies pp
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c79919 c79918)) v (pp c79919 c79918))


> hypdisj
=============================
Step 3

? (pp c79919 c79918)

1. (tpp c79919 c79918)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c79919 c79918)

1. (~ (pp c79919 c79918))
2. (tpp c79919 c79918)

> hyp

Show pp implies p
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c85048 c85047)) v (p c85048 c85047))


> hypdisj
=============================
Step 3

? (p c85048 c85047)

1. (pp c85048 c85047)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c85048 c85047)

1. (~ (p c85048 c85047))
2. (pp c85048 c85047)

> hyp

Transitivity of p
=============================
Step 1

? (all x (all y (all z (((p x y) & (p y z)) => (p x z)))))


> revsk
=============================
Step 2

? (((~ (p c90235 c90234)) v (~ (p c90234 c90233))) v (p c90235 c90233))


> hypdisj
=============================
Step 3

? (p c90235 c90233)

1. (p c90234 c90233)
2. (p c90235 c90234)

> ((p Z X) <-- (~ (c (f85078 Z X Y) Z)))
=============================
Step 4

? (~ (c (f85078 c90235 c90233 Var33) c90235))

1. (~ (p c90235 c90233))
2. (p c90234 c90233)
3. (p c90235 c90234)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 5
|
|? (p c90235 Var36)
|
|1. (c (f85078 c90235 c90233 Var33) c90235)
|2. (~ (p c90235 c90233))
|3. (p c90234 c90233)
|4. (p c90235 c90234)
|
|> hyp
=============================
Step 6

? (~ (c (f85078 c90235 c90233 Var33) c90234))

1. (c (f85078 c90235 c90233 Var33) c90235)
2. (~ (p c90235 c90233))
3. (p c90234 c90233)
4. (p c90235 c90234)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 7
|
|? (p c90234 Var40)
|
|1. (c (f85078 c90235 c90233 Var33) c90234)
|2. (c (f85078 c90235 c90233 Var33) c90235)
|3. (~ (p c90235 c90233))
|4. (p c90234 c90233)
|5. (p c90235 c90234)
|
|> hyp
=============================
Step 8

? (~ (c (f85078 c90235 c90233 Var33) c90233))

1. (c (f85078 c90235 c90233 Var33) c90234)
2. (c (f85078 c90235 c90233 Var33) c90235)
3. (~ (p c90235 c90233))
4. (p c90234 c90233)
5. (p c90235 c90234)

> ((~ (c (f85078 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 9

? (~ (p c90235 c90233))

1. (c (f85078 c90235 c90233 Var33) c90233)
2. (c (f85078 c90235 c90233 Var33) c90234)
3. (c (f85078 c90235 c90233 Var33) c90235)
4. (~ (p c90235 c90233))
5. (p c90234 c90233)
6. (p c90235 c90234)

> hyp

So tpp-tpp implies p via trans
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (tpp y z)) => (p x z)))))


> revsk
=============================
Step 2

? (((~ (tpp c95578 c95577)) v (~ (tpp c95577 c95576))) v (p c95578 c95576))


> hypdisj
=============================
Step 3

? (p c95578 c95576)

1. (tpp c95577 c95576)
2. (tpp c95578 c95577)

> ((p X Z) <-- (p X Y) (p Y Z))
|=============================
|Step 4
|
|? (p c95578 Var32)
|
|1. (~ (p c95578 c95576))
|2. (tpp c95577 c95576)
|3. (tpp c95578 c95577)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 5
|
|? (pp c95578 Var32)
|
|1. (~ (p c95578 Var32))
|2. (~ (p c95578 c95576))
|3. (tpp c95577 c95576)
|4. (tpp c95578 c95577)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 6
|
|? (tpp c95578 Var32)
|
|1. (~ (pp c95578 Var32))
|2. (~ (p c95578 Var32))
|3. (~ (p c95578 c95576))
|4. (tpp c95577 c95576)
|5. (tpp c95578 c95577)
|
|> hyp
=============================
Step 7

? (p c95577 c95576)

1. (~ (p c95578 c95576))
2. (tpp c95577 c95576)
3. (tpp c95578 c95577)

> ((p X Y) <-- (pp X Y))
=============================
Step 8

? (pp c95577 c95576)

1. (~ (p c95577 c95576))
2. (~ (p c95578 c95576))
3. (tpp c95577 c95576)
4. (tpp c95578 c95577)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 9

? (tpp c95577 c95576)

1. (~ (pp c95577 c95576))
2. (~ (p c95577 c95576))
3. (~ (p c95578 c95576))
4. (tpp c95577 c95576)
5. (tpp c95578 c95577)

> hyp

So also implies pp by pp def
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (tpp y z)) => (pp x z)))))


> revsk
=============================
Step 2

? (((~ (tpp c101077 c101076)) v (~ (tpp c101076 c101075))) v (pp c101077 c101075))


> hypdisj
=============================
Step 3

? (pp c101077 c101075)

1. (tpp c101076 c101075)
2. (tpp c101077 c101076)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c101077 c101075)
|
|1. (~ (pp c101077 c101075))
|2. (tpp c101076 c101075)
|3. (tpp c101077 c101076)
|
|> ((p X Z) <-- (tpp X Y) (tpp Y Z))
||=============================
||Step 5
||
||? (tpp c101077 Var41)
||
||1. (~ (p c101077 c101075))
||2. (~ (pp c101077 c101075))
||3. (tpp c101076 c101075)
||4. (tpp c101077 c101076)
||
||> hyp
|=============================
|Step 6
|
|? (tpp c101076 c101075)
|
|1. (~ (p c101077 c101075))
|2. (~ (pp c101077 c101075))
|3. (tpp c101076 c101075)
|4. (tpp c101077 c101076)
|
|> hyp
=============================
Step 7

? (~ (p c101075 c101077))

1. (~ (pp c101077 c101075))
2. (tpp c101076 c101075)
3. (tpp c101077 c101076)

> ((~ (p Y X)) <-- (p X Z) (~ (p Y Z)))
|=============================
|Step 8
|
|? (p c101077 Var46)
|
|1. (p c101075 c101077)
|2. (~ (pp c101077 c101075))
|3. (tpp c101076 c101075)
|4. (tpp c101077 c101076)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 9
|
|? (pp c101077 Var46)
|
|1. (~ (p c101077 Var46))
|2. (p c101075 c101077)
|3. (~ (pp c101077 c101075))
|4. (tpp c101076 c101075)
|5. (tpp c101077 c101076)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 10
|
|? (tpp c101077 Var46)
|
|1. (~ (pp c101077 Var46))
|2. (~ (p c101077 Var46))
|3. (p c101075 c101077)
|4. (~ (pp c101077 c101075))
|5. (tpp c101076 c101075)
|6. (tpp c101077 c101076)
|
|> hyp
=============================
Step 11

? (~ (p c101075 c101076))

1. (p c101075 c101077)
2. (~ (pp c101077 c101075))
3. (tpp c101076 c101075)
4. (tpp c101077 c101076)

> ((~ (p Y X)) <-- (pp X Y))
=============================
Step 12

? (pp c101076 c101075)

1. (p c101075 c101076)
2. (p c101075 c101077)
3. (~ (pp c101077 c101075))
4. (tpp c101076 c101075)
5. (tpp c101077 c101076)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 13

? (tpp c101076 c101075)

1. (~ (pp c101076 c101075))
2. (p c101075 c101076)
3. (p c101075 c101077)
4. (~ (pp c101077 c101075))
5. (tpp c101076 c101075)
6. (tpp c101077 c101076)

> hyp

Decompose pp into tpp or ntpp
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c106730 c106729)) v ((tpp c106730 c106729) v (ntpp c106730 c106729)))


> hypdisj
=============================
Step 3

? (ntpp c106730 c106729)

1. (~ (tpp c106730 c106729))
2. (pp c106730 c106729)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f101174 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c106730 c106729)
|
|1. (~ (ntpp c106730 c106729))
|2. (~ (tpp c106730 c106729))
|3. (pp c106730 c106729)
|
|> hyp
=============================
Step 5

? (~ (ec (f101174 c106730 c106729 Var32) c106730))

1. (~ (ntpp c106730 c106729))
2. (~ (tpp c106730 c106729))
3. (pp c106730 c106729)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c106730 Var36)
||
||1. (ec (f101174 c106730 c106729 Var32) c106730)
||2. (~ (ntpp c106730 c106729))
||3. (~ (tpp c106730 c106729))
||4. (pp c106730 c106729)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f101174 c106730 c106729 Var32) c106729)
|
|1. (ec (f101174 c106730 c106729 Var32) c106730)
|2. (~ (ntpp c106730 c106729))
|3. (~ (tpp c106730 c106729))
|4. (pp c106730 c106729)
|
|> ((ec (f101174 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c106730 c106729))
||
||1. (~ (ec (f101174 c106730 c106729 Var32) c106729))
||2. (ec (f101174 c106730 c106729 Var32) c106730)
||3. (~ (ntpp c106730 c106729))
||4. (~ (tpp c106730 c106729))
||5. (pp c106730 c106729)
||
||> hyp
|=============================
|Step 9
|
|? (pp c106730 c106729)
|
|1. (~ (ec (f101174 c106730 c106729 Var32) c106729))
|2. (ec (f101174 c106730 c106729 Var32) c106730)
|3. (~ (ntpp c106730 c106729))
|4. (~ (tpp c106730 c106729))
|5. (pp c106730 c106729)
|
|> hyp
=============================
Step 10

? (~ (tpp c106730 c106729))

1. (ec (f101174 c106730 c106729 Var32) c106730)
2. (~ (ntpp c106730 c106729))
3. (~ (tpp c106730 c106729))
4. (pp c106730 c106729)

> hyp

Finally prove main theorem

=============================
Step 1

? (((tpp a b) & (tpp b c)) => ((tpp a c) v (ntpp a c)))


> revsk
=============================
Step 2

? (((~ (tpp a b)) v (~ (tpp b c))) v ((tpp a c) v (ntpp a c)))


> hypdisj
=============================
Step 3

? (ntpp a c)

1. (~ (tpp a c))
2. (tpp b c)
3. (tpp a b)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp a c)
|
|1. (~ (ntpp a c))
|2. (~ (tpp a c))
|3. (tpp b c)
|4. (tpp a b)
|
|> ((pp X Z) <-- (tpp X Y) (tpp Y Z))
||=============================
||Step 5
||
||? (tpp a Var29)
||
||1. (~ (pp a c))
||2. (~ (ntpp a c))
||3. (~ (tpp a c))
||4. (tpp b c)
||5. (tpp a b)
||
||> hyp
|=============================
|Step 6
|
|? (tpp b c)
|
|1. (~ (pp a c))
|2. (~ (ntpp a c))
|3. (~ (tpp a c))
|4. (tpp b c)
|5. (tpp a b)
|
|> hyp
=============================
Step 7

? (~ (tpp a c))

1. (~ (ntpp a c))
2. (~ (tpp a c))
3. (tpp b c)
4. (tpp a b)

> hyp
